The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, l)) → s(length(l))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
head(cons(x, l)) → x
head(nil) → undefined
tail(nil) → nil
tail(cons(x, l)) → l
reverse(l) → rev(0, l, nil, l)
rev(x, l, accu, orig) → if(lt(x, length(orig)), x, l, accu, orig)
if(true, x, l, accu, orig) → rev(s(x), tail(l), cons(head(l), accu), orig)
if(false, x, l, accu, orig) → accu

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, l)) → s(length(l))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
head(cons(x, l)) → x
head(nil) → undefined
tail(nil) → nil
tail(cons(x, l)) → l
reverse(l) → rev(0, l, nil, l)
rev(x, l, accu, orig) → if(lt(x, length(orig)), x, l, accu, orig)
if(true, x, l, accu, orig) → rev(s(x), tail(l), cons(head(l), accu), orig)
if(false, x, l, accu, orig) → accu

S is empty.
Rewrite Strategy: FULL

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
length(cons(x, l)) →⁺ s(length(l))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [l / cons(x, l)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)